Elaborating where clauses directly in the logic #49

scalexm · 2017-06-14T20:02:28Z

These commits aim at implementing the additional rules described in #12 for elaborating where clauses
directly in the logic. Basically, each where clause of the form T: Foo expands to T: Foo, WF(T: Foo)
and each where clause of the form T: Foo<Item = U> expands to T: Foo<Item = U>, T: Foo, WF(T: Foo).
We also added reverse rules on traits and associated types, and well-formedness checking of struct
parameters and fields.

Also, the where_clauses field on AssociatedTyDatum was removed since this can be emulated by writing:

trait Item where <Self as Item>::Out: Eq {
    type Out;
}

Traits

The rules generated by a trait declaration are:

trait Bar { }
// WF(?Self: Bar) :- WF(?Self)

trait Foo<T> where T: Bar { }
// WF(?Self: Foo<?T>) :- WF(?Self), WF(?T), (?T: Bar), WF(?T: Bar)

// "Reverse" rules
// (?T: Bar) :- WF(?Self: Foo<?T>)
// WF(?T: Bar) :- WF(?Self: Foo<?T>)

Structs

The rules generated by a struct declaration are:

trait Clone { }
struct Bar { }

struct Foo<T, U> where T: Clone { }
// WF(Foo<?T, ?U>) :- WF(?T), (T: Clone), WF(?T: Clone)

Impls

The rules generated by an impl declaration are:

trait Clone { }
trait Foo<T> { }
struct X { }

impl Foo<T> for X where T: Clone { }
// (X: Foo<?T>) :- (?T: Clone), WF(?T: Clone)
// no need to check WF(?T) because this will be required by WF(X: Foo<?T>)

Associated types

The rules generated by an associated type definition are:

trait Foo {
    type Assoc;
}
// <?T as Foo>::Assoc ==> (Foo::Assoc)<?T> :- (?T: Foo)
// forall<U> { (?T: Foo) :- <?T as Foo>::Assoc ==> U }

nikomatsakis

This is a partial review -- I didn't get a chance to finish everything. =)

nikomatsakis · 2017-06-16T23:34:13Z

src/lower/mod.rs

        //
        // we generate the following clause:
        //
-        //    for<?T> WF(Foo<?T>) :- (?T: Eq).
+        //    for<?T> WF(Foo<?T>) :- WF(?T), WF(Bar), (?T: Eq), WF(?T: Eq).


Hmm, I don't think we want to include WF(Bar) in this list. That is, I think that WF(Foo<T>) is just saying if a reference to the type Foo<T> is well-formed. Not if the struct definition is well-formed -- for the latter, I would expect us to generate some rules like:

StructDefnWf(Foo) :- for<T> { if (T: Eq) { WF(Bar) } }.

I'm not sure to understand, when would we use WF(Foo<T>) and ˋStructDefnWF`?

We would never use StructDefnWF. Rather, StructDefnWF would be one of the things we must prove to decide if the whole program type-checks. This is basically a modularity thing -- it's the same as saying that if you have some function foo, we just need its signature to type-check the callers, but then we separately type-check the body of foo against its signature.

Here, the idea is that, for some struct S, the users of S need not know the types of its fields; they can assume that if the type S is well-formed, then the types of its fields are well-formed.

Yeah ok I see!

nikomatsakis · 2017-06-16T23:39:59Z

src/solve/test.rs

@@ -175,7 +175,7 @@ fn prove_forall() {
        // Here, we do know that `T: Clone`, so we can.
        goal {
            forall<T> {
-                if (T: Clone) {
+                if (WellFormed(T: Clone), T: Clone) {


Man. I have to review the plan. I sort of forget why we need the WF's again. ;)

Yeah I was waiting for your review here

Basically given:

trait Clone { } impl<T> Clone for Vec<T> where T: Clone { }

we need to generate (Vec<T>: Clone) :- (T: Clone), WF(T: Clone)

because of this example:

trait Clone where Self: Marker { } impl<T> Clone for Vec<T> where T: Clone { }

here we need to have WF(T: Clone) in order to have Vec<T>: Clone because WF(T: Clone) implies that T correctly implements Marker whereas this is not the case with the assumption T: Clone alone

Yes. So I wonder if it's worth having two forms -- e.g., if and if-raw or something -- where the former "elaborates" so that T: Clone is "short" for WF(T: Clone), T: Clone, just as it would be in an impl. It seems useful to be able to suppress that elaboration, but I imagine that we'll almost always want it to happen, no?

I thought about this indeed, and I'm in favor of adding an if_raw.

nikomatsakis · 2017-06-16T23:41:07Z

src/solve/test.rs

        }

        goal {
            forall<T, U> {
-                if (T: Item<Out = U>) {
+                if (WellFormed(T: Item), T: Item<Out = U>) {


why is this WF(T: Item) and not WF(T: Item<Out = U>)? Because the former suffices?

Here indeed the former suffices. At first I thought we didn't need something like WF(Projection). But now that you say it, there's indeed no way to have something like that:

trait Foo where <Self as Foo>::Item: Eq { type Item; } if (WellFormed(T: Foo<Item = Bar>)) { ... }

Currently, we have to add T: Foo<Item = Bar> into the environment in order to trigger the normalization, and rely on WF(T: Foo). But as a consequence we are also pushing T: Foo into the environnement (it is implied by T: Foo<Item = Bar>) so basically we are making a stronger hypothesis that initially wanted.
It may be not so difficult to fix however.

nikomatsakis · 2017-06-28T10:10:08Z

Sorry for delay @scalexm ! Will try to wrap this up ASAP.

scalexm · 2017-06-30T19:11:54Z

We also need more reverse rules, like:

struct S<T> where T: Clone { }
// current:
// WF(S<T>) :- T: Clone, WF(T: Clone)
//
// should add:
// (T: Clone) :- WF(S<T>)
// WF(T: Clone) :- WF(S<T>)

impl<T> Foo for T { }
// current:
// WF(T: Foo) :- WF(T)
//
// should add:
// WF(T) :- WF(T: Foo)

nikomatsakis · 2017-07-07T14:22:49Z

src/lower/mod.rs

+                                     .iter()
+                                     .cloned()
+                                     .flat_map(|wc| wc.expanded(program))
+                                     .map(|wc| wc.cast())


apropos of nothing, we should make a .casted() adapter just to make this cuter :)

Yeah right!

nikomatsakis

I think that to land this PR we should, at minimum, tweak the handling of struct fields and well-formedness. I'd also like to see a test that we get an error when the user fails to provide the full set of impls (if there is already such a test, my bad, I missed it). Something like this:

trait Foo: Bar { }
trait Bar { }
struct A { }
impl Foo for A { } // NB: No impl of Bar for A

and then a query that WF(A: Foo) ought to fail, right? (Even though A: Foo would succeed.) I think this is the basic idea we were going for.

Other things that we could do in this PR, but maybe would be better left for a follow-up:

Elaborate the clauses in an if, which would also eliminate some portion of the diffs.
Consider adding an "unelaborated" form, though we could wait until we need it.
- These would lower to the same thing, presumably, so the difference is just skin-deep.

scalexm · 2017-07-09T18:58:13Z

chalk-parse/src/parser.lalrpop

@@ -28,7 +28,8 @@ pub Goal: Box<Goal> = {
 Goal1: Box<Goal> = {
    "forall" "<" <p:Comma<ParameterKind>> ">" "{" <g:Goal> "}" => Box::new(Goal::ForAll(p, g)),
    "exists" "<" <p:Comma<ParameterKind>> ">" "{" <g:Goal> "}" => Box::new(Goal::Exists(p, g)),
-    "if" "(" <w:Comma<WhereClause>> ")" "{" <g:Goal> "}" => Box::new(Goal::Implies(w, g)),
+    "if" "(" <w:Comma<WhereClause>> ")" "{" <g:Goal> "}" => Box::new(Goal::Implies(w, g, true)),
+    "if_raw" "(" <w:Comma<WhereClause>> ")" "{" <g:Goal> "}" => Box::new(Goal::Implies(w, g, false)),


@nikomatsakis, do you have an idea of how I could factorize these two lines?

not sure you need to, but you could do:

Goal1: Box<Goal> = { ... <i:IfKeyword> ... => Box::new(Goal::Implies(w, g, i)), }; IfKeyword: bool = { "if" => true, "if_raw" => false, };

(if that generates conflicts, you can add #[inline] onto the IfKeyword, but I can't see why it would)

Great, that's what I was looking for

scalexm · 2017-07-09T19:08:57Z

src/lower/mod.rs

+                    });
+                }
+                Ok(Box::new(ir::Goal::Implies(where_clauses, g.lower(env)?)))
+            }


@nikomatsakis not sure about using ir::with_current_program, basically it prevents from having user provided higher ranked bounds like where if (I: Iterator<Item = U>) { U: Eq } (but we don't support them).

hmm -- seems ok for now -- we can revisit at a later point if we ever care, I think.

Really all we need is enough data to know how many parameters are declared on trait vs associated types. I think eventually we are going to have to refactor to support a more general "query-style" lowering, like rustc does, which should enable us to uncover that data without full access to other things. But, as you say, for now we don't support hypotheses in user-defined goals anyhow... (though it seems like we may want that eventually)

nikomatsakis · 2017-07-10T14:46:51Z

src/cast.rs

@@ -130,7 +131,7 @@ impl<T, U> Cast<Vec<U>> for Vec<T>
    where T: Cast<U>
 {
    fn cast(self) -> Vec<U> {
-        self.into_iter().map(|v| v.cast()).collect()
+        self.into_iter().casted().collect()


nikomatsakis

looks great; just one comment would be nice

nikomatsakis · 2017-07-10T14:48:23Z

src/lower/mod.rs

+                    });
+                }
+                Ok(Box::new(ir::Goal::Implies(where_clauses, g.lower(env)?)))
+            }


hmm -- seems ok for now -- we can revisit at a later point if we ever care, I think.

nikomatsakis · 2017-07-10T14:49:14Z

src/solve/test.rs

                    Vec<T>: Clone
                }
            }
        } yields {
            "Unique; substitution [], lifetime constraints []"
        }
+
+        goal {


maybe good to add a comment here that we are explicitly not "knowing" that WF(T: Clone), right?

nikomatsakis · 2017-07-10T14:49:46Z

src/solve/test.rs

            Slice<Int>: Eq<Slice<Int>>
        } yields {
            "No possible solution"
        }

-        // not WF because previous equation doesn't hold
+        // not WF because previous equation doesn't hold, despite Slice<Int> having an impl for Ord<Int> 


nikomatsakis · 2017-07-10T14:55:35Z

Rebased, added comment.

nikomatsakis reviewed Jun 16, 2017

View reviewed changes

nikomatsakis reviewed Jul 7, 2017

View reviewed changes

nikomatsakis requested changes Jul 7, 2017

View reviewed changes

scalexm commented Jul 9, 2017

View reviewed changes

scalexm force-pushed the elaborate branch 2 times, most recently from 58365b7 to fdcf099 Compare July 10, 2017 09:25

nikomatsakis reviewed Jul 10, 2017

View reviewed changes

nikomatsakis requested changes Jul 10, 2017

View reviewed changes

nikomatsakis approved these changes Jul 10, 2017

View reviewed changes

scalexm and others added 6 commits July 10, 2017 10:55

Elaborate where clauses directly in the logic

7ce7cb0

Add some documentation

a51a25b

Add WF checks for struct fields

7e39323

Remove WF checks for struct fields

bafd6f3

Elaborate where clauses in Implies goals

444f6e1

add comment about if_raw

dd6f707

nikomatsakis force-pushed the elaborate branch from 01ab17e to dd6f707 Compare July 10, 2017 14:55

More concise grammar

6345f7d

nikomatsakis approved these changes Jul 10, 2017

View reviewed changes

nikomatsakis merged commit 07f713e into rust-lang:master Jul 10, 2017

scalexm deleted the elaborate branch July 10, 2017 15:30

scalexm mentioned this pull request Jul 13, 2017

Auto traits #54

Merged

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Elaborating where clauses directly in the logic #49

Elaborating where clauses directly in the logic #49

scalexm commented Jun 14, 2017 •

edited

Loading

nikomatsakis left a comment

nikomatsakis Jun 16, 2017

scalexm Jun 17, 2017

nikomatsakis Jun 28, 2017

scalexm Jun 28, 2017

nikomatsakis Jun 16, 2017

scalexm Jun 17, 2017 •

edited

Loading

scalexm Jun 28, 2017

nikomatsakis Jul 7, 2017

scalexm Jul 9, 2017

nikomatsakis Jun 16, 2017

scalexm Jun 17, 2017

nikomatsakis commented Jun 28, 2017

scalexm commented Jun 30, 2017

nikomatsakis Jul 7, 2017

scalexm Jul 9, 2017

nikomatsakis left a comment

scalexm Jul 9, 2017

nikomatsakis Jul 10, 2017

nikomatsakis Jul 10, 2017

scalexm Jul 10, 2017

scalexm Jul 9, 2017 •

edited

Loading

nikomatsakis Jul 10, 2017

nikomatsakis Jul 10, 2017

nikomatsakis Jul 10, 2017

nikomatsakis left a comment

nikomatsakis Jul 10, 2017

nikomatsakis Jul 10, 2017

nikomatsakis Jul 10, 2017

nikomatsakis commented Jul 10, 2017

Elaborating where clauses directly in the logic #49

Elaborating where clauses directly in the logic #49

Conversation

scalexm commented Jun 14, 2017 • edited Loading

Traits

Structs

Impls

Associated types

nikomatsakis left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

scalexm Jun 17, 2017 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

nikomatsakis commented Jun 28, 2017

scalexm commented Jun 30, 2017

Choose a reason for hiding this comment

Choose a reason for hiding this comment

nikomatsakis left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

scalexm Jul 9, 2017 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

nikomatsakis left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

nikomatsakis commented Jul 10, 2017

scalexm commented Jun 14, 2017 •

edited

Loading

scalexm Jun 17, 2017 •

edited

Loading

scalexm Jul 9, 2017 •

edited

Loading